#include <iostream>
#include <stdlib.h>

#include "atom.h"
#include "bind.h"
#include "generalizer.h"
#include "predicates.h"
#include "prover.h"
#include "system.h"
#include "tree.h"
#include "tuple.h"

class assertCall : public OnceProver {
predicateName("assert")

  bool proveOnce () {
    pNode node = excludeFirst (*tuple);
    system->rules.assertz (node);
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<assertCall, Tuple::ID> assertRegistrar;

class ShortAssert : public assertCall { // @ is a shortcut to assert
predicateName("@")
  ;
};

ProverFactoryRegistrar<ShortAssert, Tuple::ID> shortAssertRegistrar;

// Is the whole clause bounded?
bool isWholeBounded (Node &node) {
  Node &finalNode = *node.final ();
  switch(finalNode.type ()) {
  case Reference::ID:
    return false;
  case Atom::ID:
  case String::ID:
  case Number::ID:
    return true;
  case Tree::ID: {
    Tree &tree = static_cast<Tree&> (finalNode);
    return isWholeBounded (*tree.left) && isWholeBounded (*tree.right);
  }
  case Tuple::ID: {
    Tuple &tuple = static_cast<Tuple&> (finalNode);
    for(std::vector<pNode>::iterator p = tuple.nodes.begin (); p
        < tuple.nodes.end (); p++)
      if(!isWholeBounded (**p))
        return false;

    return true;
  }
  }
  return false;
}

class bound : public OnceProver {
predicateName("bound")

  bool proveOnce () {
    return typeid(*tuple->nodes[1].final ()) != typeid(Reference);
  }

  Tuple *tuple;
  void set (Tuple &t, System&) {
    tuple = &t;
  }
};

ProverFactoryRegistrar<bound, Tuple::ID, 2> boundRegistrar;

class Equate : public OnceBindProver {
predicateName("=")

  bool proveOnce () {
    return binder.bind (*tree->left, *tree->right, system->trail);
  }

  Tree *tree;
  void set (Tree &t, System &s) {
    tree = &t;
    OnceBindProver::set (s);
  }
};

ProverFactoryRegistrar<Equate, Tree::ID> EquateRegistrar;

class exec : public OnceBindTupleProver {
predicateName("exec")

  bool proveOnce () {
    if(tuple->nodes.size () > 3)
      return false;

    int result = ::system (tuple->nodes[1].node->display ().c_str ());

    if(tuple->nodes.size () > 2)
      return binder.bind (*tuple->nodes[2], *Number::create (result),
          system->trail);
    else
      return (result == 0);
  }
};

ProverFactoryRegistrar<exec, Tuple::ID> execRegistrar;

class generalizeCall : public OnceBindTupleProver {
predicateName("generalize")

  bool proveOnce () {
    return binder.bind (*generalize (*tuple->nodes[1]), *tuple->nodes[2],
        system->trail);
  }
};

ProverFactoryRegistrar<generalizeCall, Tuple::ID, 3> generalizeRegistrar;

class infixCall : public OnceBindTupleProver {
predicateName("infix")

  bool proveOnce () {
    Node *treeNode = tuple->nodes[1].final (),
      *opNode = tuple->nodes[3].final ();

    if(typeid(*opNode) == typeid(Reference))
      if(typeid(*treeNode) == typeid(Tree)) {
        Tree &tree = static_cast<Tree&> (*treeNode);
        char *ops = tree.ops;
        pNode atom = new String (std::string (ops, ops[1] == 0 ? 1 : 2));
        return binder.bind (*opNode, *atom, system->trail) &&
          binder.bind (*tuple->nodes[2], *tree.left, system->trail) &&
          binder.bind (*tuple->nodes[4], *tree.right, system->trail);
      } else
        return false;
    else {
      pNode tree = new Tree (opNode->display ().c_str (),
          tuple->nodes[2], tuple->nodes[4]);
      return binder.bind (*tree, *tuple->nodes[1], system->trail);
    }
  }
};

ProverFactoryRegistrar<infixCall, Tuple::ID, 5> infixRegistrar;

class list : public OnceProver {
predicateName("list")

  list () :
    tuple (0) {
  }
  bool proveOnce () {
    bool filter;
    std::string search;

    filter = tuple != 0;
    if(filter)
      search = Prototype::get (*tuple->nodes[1]).functorName ();

    RulesIterator *iterator = system->rules.createIteratorForAll ();
    Node *rule;
    Prototype proto, prevProto; // For a fancy blank line

    for(; iterator->valid (); iterator->next ()) {
      rule = **iterator;
      proto = Prototype::getFromRule (*rule);

      if(!filter || proto.functorName () == search) {
        if(proto != prevProto) {
          std::cout << std::endl;
          prevProto = proto;
        }
        std::cout << rule->dump () << ' ' << endOfRuleMarker << std::endl;
      }
    }

    delete iterator;
    return true;
  }

  Tuple *tuple;
  System *system;
  void set (Atom&, System &s) {
    system = &s;
  }
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<list, Atom::ID> listRegistrar;
ProverFactoryRegistrar<list, Tuple::ID, 2> listPredicateRegistrar;

class quit : public OnceProver { // Exit abruptly
predicateName("quit")

  bool proveOnce () {
    int ret = 0;
    if(tuple && tuple->nodes.size () == 2) {
      Node &final = *tuple->nodes[1].final ();
      if(typeid(final) == typeid(Number))
        ret = static_cast<Number&> (final).value;
    }

    exit (ret);
    // Not even true or false
  }

  Tuple *tuple;
  void set (Atom&, System&) {
    tuple = 0;
  }
  void set (Tuple &t, System&) {
    tuple = &t;
  }
};

ProverFactoryRegistrar<quit, Atom::ID> quitRegistrar;
ProverFactoryRegistrar<quit, Tuple::ID> quitWithCodeRegistrar;

class retract : public Prover {
predicateName("retract")

  retract () :
    firstRun (true) {
  }

  bool prove () {
    Node *rule = tuple->nodes[1].node;
    if(firstRun)
      binder.capture (system->trail);
    else
      binder.undo (system->trail);

    RulesIterator *rulesIterator;
    for(rulesIterator = system->rules.createIterator (Prototype::getFromRule (
        *rule)); rulesIterator->valid (); rulesIterator->next ())
      if(binder.bind (***rulesIterator, *rule, system->trail)) {

        // After deletion, next item is shifted to current - is it true?
        // rulesIterator->next ();

        system->rules.retract (**rulesIterator);
        delete rulesIterator;
        return true;
      }

    delete rulesIterator;
    return false;
  }

  bool firstRun;
  Binder binder;
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<retract, Tuple::ID, 2> retractRegistrar;

class rule : public Prover {
predicateName("rule")

  rule () :
    rulesIterator (0) {
  }
  ~rule () {
    if(rulesIterator)
      delete rulesIterator;
  }

  bool prove () {
    if(!rulesIterator) { // First run
      binder.capture (system->trail);
      rulesIterator = system->rules.createIterator (Prototype::getFromRule (
          *tuple->nodes[1]));
      last = 0;
    } else
      binder.undo (system->trail);

    if(!rulesIterator->valid ()) return false;

    while(true) {

      // Do not advance if first rule, or if current rule is retracted
      if(last && **rulesIterator == last) {
        rulesIterator->next ();
        if(!rulesIterator->valid ()) return false;
      }
      last = **rulesIterator;

      if(binder.bind (*last, *tuple->nodes[1], system->trail))
        return true;
    }

    return false;
  }

  RulesIterator *rulesIterator;
  Node *last;
  Binder binder;
  Tuple *tuple;
  System *system;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<rule, Tuple::ID, 2> ruleRegistrar;
